COMMENT ⊗   VALID 00013 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.require "memo.pub[let,jmc]" source
C00005 00003	.bb "#. Introduction and Motivation."
C00009 00004	.bb "#. Recursive Programs."
C00012 00005	.bb "#. The Functional Equation of a Recursive Program."
C00017 00006	.bb "#. First Order Axioms for Lisp."
C00025 00007	.bb "#. An Extended Example."
C00036 00008	.bb "#. The Minimization Schema."
C00044 00009	.bb "#. Proof Methods as Axiom Schemata"
C00052 00010	.bb "#. Representations Using Finite Approximations."
C00064 00011	.BB "#. Questions of Incompleteness."
C00071 00012	.bb "#. References."
C00074 00013	.skip 1
C00075 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.every heading (REPRESENTATION,...draft...,{page})
.font B "zero30"
.AT "qt" ⊂"%At%*"⊃
.AT "qf" ⊂"%Af%*"⊃
.AT "qw" ⊂"%8T%*"⊃
.at "Goedel" ⊂"G%B:%*odel"⊃
.at "q≤" ⊂"%8b%*"⊃
.at "q≥" ⊂"%8d%*"⊃
.select 1
.skip 15

.cb REPRESENTATION OF RECURSIVE PROGRAMS IN FIRST ORDER LOGIC

.cb by John McCarthy
.skip 10


	This paper presents methods of representing recursive programs by
sentences and schemata of first order logic, characterization of
%2recursion induction%1, %2subgoal induction%1, %2inductive assertions%1
and other ways of proving facts about programs as axiom schemata of first
order logic, and applications of these results to proving assertions about
programs.

.turn on "{"
%7This draft of
FIRST.NEW[W77,JMC]
PUBbed at {time} on {date}.%1

.skip to column 1
.bb "#. Introduction and Motivation."

	It has been concluded from the undecideability of both equivalence
and non-equivalence of abstract recursive program schemata that recursive
programs cannot be characterized in first order logic.  Cooper (1969)
showed how to characterize them in second order logic, and that seemed to
settle the matter.  However, we will exhibit first order characterizations
that are incomplete only in that they admit non-standard models like those
of first order arithmetic.  It now seems likely that all "ordinary"
%2extensional%1
assertions about programs will be provable or disprovable in first order
theories.  %2Extensional%1 assertions about a program concern the functions
computed by the program and not the manner of computation.  That a merge sort
program gives the same result as a bubble sort program is an
extensional assertion, but the fact that it does less computation is not.

	Besides illuminating the logical structure of computer programs,
these results have practical significance.  First, the correctness of
a computer program often involves facts about other mathematical domains,
and these are often conveniently expressed in first order logic or in a
set theory axiomatized in first order logic.  It has proved particularly
difficult to work within logics that admit only continuous functions and
predicates.  Second, proof-checking and theorem proving programs have been
developed for first order logic.  Finally, first order logic is complete,
so that the Goedelian incompleteness of any theory is in the set of axioms
and can be reduced when necessary by adding axioms rather than by changing
the logical system.

	While our goal is first order representations of recursive
programs, we will make considerable informal use of higher order
functionals and predicates.

	We present two methods of representing recursive programs.  The
first involves a %2functional equation%1 and a %2minimization schema%1 for
each program.  The functional equation has the function on both sides of
an equality sign and so defines it implicitly.  However, all variables are
universally quantified.  The second approach defines the function
explicitly, but existential quantifiers asserting the existence of finite
approximations to the function occur in the formula.  The fact that the
functional equation of a program not known to terminate can nevertheless
be written so simply in first order logic was discovered by
Cartwright (1977), but the rest seems new.
.bb "#. Recursive Programs."

	An adequate background for this paper is contained in (Manna 1974)
and more concisely in (Manna, Ness and Vuillemin 1973).  The connections
of recursive programs with second order logic are given in (Cooper 1969)
and (Park 1970).

	We consider %2recursive programs%1 of the form

!!g1:	%2f(x) ← %At%*[f](x)%1,

where %At%* is a %2computable functional%1 like

!!g2:	%2%At%* = λf.λx.(qif x = 0 qthen 1 qelse x . f(x - 1))%1,

which gives rise to the well known recursive definition of the factorial
function, namely

!!g3:	%2n! ← qif n = 0 qthen 1 qelse n . (n - 1)!%1.

	In general, we shall be interested in partial functions from a
domain D1 to a domain D2.  We augment these
domains by an undefined element called qw (read "bottom")
giving rise to domains D1%5+%*
and D2%5+%*.  A set ⊗F of total base functions on the domains is assumed
available, and we study functions %2computable from the set F%1
as in (McCarthy 1963).

	It is necessary to distinguish between a program as a
text and the partial function defined by the program when one is
interested in describing the dependence of the function on the
interpretation of the basic function and predicate symbols.  However, we
will be working with just one interpretation at a time, so we won't use
separate symbols for programs and the functions they determine.
.bb "#. The Functional Equation of a Recursive Program."

	Consider the Lisp program

!!h1:	%2subst[x,y,z] ← qif qat z qthen [qif z=y qthen x qelse z]
qelse subst[x,y,qa z] . subst[x,y,qd z]%1.

The above is in Lisp %2external%1 or %2publication%1 notation in
which _qa_%2x%1_ (bold face qa) stands for %2car[x]%1,
_qd_%2x%1_ for %2cdr[x]%1, _%2x_._y%1_
for %2cons[x,y]%1, _qat_%2x%1_ for %2atom[x]%1, _qn_%2x%1_ for %2null[x]%1, and
%2<x%41%2 ... x%4n%1> for %2list[x%41%2, ... ,x%4n%1], and
%2x_*_y%1 for %2append[x,y]%1.  Equality is taken as equality of
S-expressions so that qeq is not used.  The program is written

	(DE SUBST (X Y Z) (COND ((ATOM Z) (COND ((EQUAL Z Y) X) (T Z)))
(T (CONS (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z))))))

in Lisp %2internal notation%1.

	The basic functions α{%2car, cdr, cons, atomα}%1 of Lisp are all
assumed total, but we will say nothing about the values of ⊗car and
⊗cdr when applied to atoms.  According to the fixed point theory of
recursive programs, any such program defines a function ⊗f from ⊗Sexp (the
set of S-expressions) to Sexp%5+%* (the set of S-expressions augmented
by qw).  This function can be computed by any %2safe computation rule%1,
(in the terminology of Manna, Ness, and Vuillemin (1973)),
and when the computation terminates, its value will belong to ⊗Sexp.  When
the computation doesn't terminate, we postulate %2f(x)_=_qw%1.  Although
the particular function %2subst%1 always terminates,
our first order formula doesn't assume it.  Instead, the first
order formula ({eq h2}) below is the starting point of
a structural induction proof that %2subst%1 is total.

	These facts show that the function %2subst%1 defined recursively
by ({eq h1}) satisfies the sentence

!!h2:	%2∀x y z.(subst(x,y,z) = qif qat z qthen (qif z = y qthen x qelse z)
qelse subst(x,y,qa z) . subst(x,y,qd z))%1

of first order logic.  The variables %2x, y%1 and %2z%1 range over ⊗Sexp; 
when we want to quantify over %2Sexp%5+%1, we use %2X, Y %1and%2 Z%1.
Moreover, we are augmenting first order logic,
as described in (Manna 1974),
by allowing conditional
expressions as terms.  The augmentation does not change what
can be expressed in first order logic, because
conditional expressions can always be eliminated from sentences by
distributing predicates over them.  Thus ({eq h2}) can be written

!!h3:	%2∀x y z.(qat z ⊃ (z=y ⊃ subst(x,y,z) = x) ∧ z≠y ⊃ subst(x,y,z) = z)
∧ ¬qat z ⊃ subst(x,y,z) = subst(x,y,qa z) . subst(x,y,qd z)),%1

but we will use conditional expressions, because they are clearer and
express the recursive program directly.  Indeed, we recommend
their use as terms in logic generally, and in first order logic in
particular.  They don't extend the logical power, but they permit many
facts to be expressed without circumlocution.

	One goal of our first order representation is to use ({eq h1})
only to justify writing ({eq h2}) and then prove all properties of
%2subst%1 using a first order axiomatization of Lisp.
.skip 2

.bb "#. First Order Axioms for Lisp."

	We use lower case variables ⊗x, ⊗y, and ⊗z with or without
subscripts to range over S-expressions.  Capitalized variables
range over all entities.  We also use variables ⊗u, ⊗v and ⊗w with
or without subscripts to range over lists, i.e. S-expressions
such that successive %2cdr%1s eventually reach NIL.  (The %2car%1 of
a list is not required to be a list).  We use predicates %2issexp%1
and %2islist%1 to assert that an individual is an S-expression or
a list.  First come the "housekeeping" and "algebraic" axioms:

L1:	%2∀x.issexp x%1

L2:	%2∀u.islist u%1

L3:	%2∀u.issexp u%1

L4:	%2¬issexp qw

L5:	%2islist %1NIL

L6:	%2qat qNIL%1

L7:	%2∀u.(qat u ⊃ u = qnil)%1

L8:	%2∀x y.issexp (x.y)%1

L9:	%2∀x u.islist (x.u)%1

L10:	%2∀x. ¬qat x ⊃ issexp qa x%1

L11:	%2∀x. ¬qat x ⊃ issexp qd x%1

L12:	%2∀u. u ≠ qNIL ⊃ islist qd u%1

L13:	%2∀x y. qa (x.y) = x%1

L14:	%2∀x y. qd (x.y) = y%1

L15:	%2∀x y. ¬qat (x.y)%1

L16:	%2∀x.¬qat x ⊃ (qa x . qd x) = x%1

	Next we have axiom schemata of induction

LS1:	%2(∀x.qat x ⊃ %AF%* x) ∧ ∀x.(¬qat x ∧ %AF%* qa x ∧ %AF%* qd x ⊃ %AF%* x) ⊃ ∀x.%AF%* x%1

LS2:	%2(∀u.u = qnil ⊃ %AF%* u) ∧ ∀u.(u ≠ qnil ∧ %AF%* qd u ⊃ %AF%* u) ⊃ ∀u. %AF%* u%1.

	From these axioms and schemata, we can prove

!!h4:	%2∀x y z.issexp subst(x,y,z)%1

which is our way of saying that %2subst%1 is total.
The key step is applying the axiom schema LS1 with the
predicate %2%AF%*(z) ≡ issexp subst(x,y,z)%1.
We can also prove
in first order logic
such algebraic properties of %2subst%1 as

!!h5:	%2∀x y z y1 z1.(¬occur(y,z1) ⊃ subst(subst(x,y,z),y1,z1) =
subst(x,y,subst(z,y1,z1)))%1

if we have suitable axiomatization of the predicate %2occur(x,y)%1 meaning
that the atom ⊗x occurs in the S-expression ⊗y. 

	The axiomatization of the predicate %2occur%1 raises some new
problems.  It is defined by the recursive Lisp program

!!h6:	%2occur(x,y) ← (x = y) ∨ (¬qat y ∧ (occur(x,qa y) ∨ occur(x,qd y)))%1.

If we were sure in advance that %2occur%1 were total, we could translate
the recursion ({eq h6}) into the sentence

!!h7:	%2∀x y.(occur(x,y) ≡
(x = y) ∨ (¬qat y ∧ (occur(x,qa y) ∨ occur(x,qd y))))%1

which will suffice for proving ({eq h5}), but we
have no right to write it down from the recursive definition ({eq h6}).

	What we may write without proving that %2occur%1 is total
is an implicit definition

!!h8:	%2∀x y.(occura(x,y) =
(x equals y) or (not atom y and (occura(x,qa y) or occura(x,qd y))))%1

and

!!h9:	%2∀x y.(occur(x,y) ≡ (occura(x,y) = T))%1.

From ({eq h8}), we can prove that %2occura%1 is total by structural induction
and from this
({eq h7}) quickly follows.

	Since recursive definitions give rise to partial predicates,
and we don't want to use a partial predicate logic, we introduce a domain
%AP%1 of %2extended truth values%1 with characteristic predicate %2isetv%1
whose elements are ⊗T, ⊗F and qw.
There is no harm in identifying ⊗T and ⊗F with suitable Lisp atoms or
with the integers 1 and 0.
The following axioms describe
functions into or out of %AP%1.  We use the predicate %2istv%1 to test for
the honest truth values ⊗T and ⊗F. 

B1:	%2∀p.(isetv p)%1

B2:	%2∀p.(p = T ∨ p = F ∨ p = qw)%1

B3:	%2T ≠ F ∧ T ≠ qw ∧ F ≠ qw%1

B4:	%2∀p.(istv p ≡ p = T ∨ p = F)%1

B5:	%2∀p. isetv not p%1

B6:	%2∀p q. isetv(p and q)%1

B7:	%2∀p q. isetv(p or q)%1

B8:	%2∀p.(not p =
qif (p = qw) qthen qw qelse qif p = T qthen F qelse T)%1

B9:	%2∀p q.(p and q =
qif (p = qw) qthen qw qelse qif p = T qthen q qelse F)%1

B10:	%2∀p q.(p or q =
(qif p = qw) qthen qw qelse qif p = T qthen T qelse q)%1

B11:	%2∀X Y.(X equal Y = qif ¬issexp X ∨ ¬issexp Y qthen qw qelse qif
X = Y qthen T qelse F)%1

B12:	%2∀X.(aatom X =
qif ¬issexp X qthen qw qelse qif qat X qthen T qelse F)%1,

and we also need a conditional expression that can take an argument from %AP%1,
namely

B13:	%2∀p X Y.(if(p,X,Y) = qif p = qw qthen qw qelse qif p = T qthen X
qelse Y)%1.

	%2occura%1 is proved total by applying schema LS1 with
%2%AF%*(y) ≡ occura(x,y) ≠ qw%1.  After this %2occur%1 can be shown to
satisfy ({eq h7}).

	The axioms L1-L16 and B1-B12 together with the sentences arising
from the schemata LS1 and LS2 will be called the axiom system Lisp0.  We
will adjoin one more axiom later to get the system Lisp1.

	The above method of replacing a recursion by a first order
sentence was first (I think) used in (Cartwright 1977).  I'm
surprised that it wasn't invented sooner.

.skip 1
.indent 0,0;
.bb "#. An Extended Example."

	The SAMEFRINGE problem is to write a program that efficiently
determines whether two S-expressions have the same fringe, i.e. have
the same atoms in the same order.  (Some people omit the qnils at the ends
of lists, but we will take all atoms).  Thus
((A.B).C) and (A.(B.C)) have the same fringe, namely (A B C).  The
object of the original problem was to program it using a minimum of 
storage, and it was conjectured that co-routines were necessary to
do it neatly.  We shall not discuss that matter here - merely the
extensional correctness of one proposed solution.

	The relevant recursive definitions are

!!n1:	%2fringe x ← qif qat x qthen <x> qelse fringe qa x * fringe qd x%1,

where %2u_*_v%1 denotes the result of appending the lists ⊗u and ⊗v and
is defined recursively by

!!n2:	%2u * v ← qif qn u qthen v qelse qa u . [qd u * v]%1.

We are interested in the condition %2fringe x = fringe y%1.

	The function to be proved correct is %2samefringe[x,y]%1 defined by
the simultaneous recursion

!!n3:	%2samefringe[x, y] ← (x = y) ∨ [¬qat x ∧ ¬qat y ∧ same[gopher x, gopher y]]%1,

!!n4:	%2same[x, y] ← (qa x = qa y) ∧ samefringe[qd x, qd y]%1,

where

!!n5:	%2gopher x ←  qif qat qa x qthen x qelse gopher qaa x . [qda x . qd x]%1.

	We need to prove that %2samefringe%1 is total and

!!n6:	%2∀xy.(samefringe[x,y] ≡ fringe x = fringe y)%1.

	The minimization schemata of these functions are irrelevant, because
we will prove that the functions are all total except that we won't
prove anything about the result of applying %2gopher%1 to an atom.  The
functional equations are


!!n7:	%2∀x.(fringe x = qif qat x qthen <x> qelse fringe qa x * fringe qd x%1),

!!n8:	%2∀u v.(u * v = qif qn u qthen v qelse qa u . [qd u * v])%1.

!!n9:	%2∀x y.(samefringe[x, y] = x equal y
or [not aat x and not aat y and same[gopher x, gopher y]])%1,

!!n10:	%2∀x y.(same[x, y] = qa x equal qa y and samefringe[qd x, qd y]%1,

!!n11:	%2∀x.(gopher x =  qif qat qa x qthen u
qelse gopher qaa x . [qda x . qd x])%1.

Note that because ⊗samefringe and ⊗same are recursively defined predicates
which have not been proved total, their functional equations must use the
imitation propositional functions involving the extended truth values.

	We shall not give full proofs but merely the induction predicates
and a few indications of the algebraic transformations.  We begin with
a lemma about %2gopher%1.

!!n12:	%2∀x y.(issexp gopher[x.y] ∧ qat qa gopher[x.y] ∧
fringe gopher[x.y] = fringe[x.y])%1.

	This lemma can be proved by S-expression structural induction
using the predicate

!!n13:	%2P(x) ≡ ∀y.ok(x,y)%1,

where %2ok(x,y)%1 is defined by

!!n13a:	%2∀x y.(ok(x,y) ≡ issexp gopher[x.y] ∧ qat qa gopher[x.y] ∧
fringe gopher[x.y] = fringe[x.y])%1.

In the course of the proof, we use the associativity of * and the
formula %2fringe[x.y]_=_fringe_x_*_fringe_y%1.
The lemma was expressed using %2gopher[x.y]%1 in order to avoid
considering atomic arguments for %2gopher%1, but it could have
equally well be proved about %2gopher_x%1 with the condition
%2¬qat_x%1.

	Another proof can be given using the course-of-values induction
schema for integers.  We write this schema

ICV:	%2∀n.(∀m.(m < n ⊃ P(m)) ⊃ P(n)) ⊃ ∀n.P(n)%1,

.turn on "↑";
where ⊗m and ⊗n range over non-negative integers.  Exactly the same
schema expresses transfinite induction; we need only imagine the
variables ranging over all ordinals less than a given one - in this
case %Aw%1, but equally well %Aw↑w%1 or ε%40%1.
We also use the function %2size_x%1 defined by

!!n14:	%2size x ← qif qat x qthen 1 qelse size qa x + size qd x%1

satisfying the obvious functional equation.
Our induction predicate is then

!!n15:	%2P(n) ≡ ∀x y.(size x = n ⊃ ok(x,y))%1.

	
	For our proof about %2samefringe%1 we need one more lemma
about %2gopher%1, namely

!!n16:	%2∀x y.(size gopher[x.y] = size[x.y]%1.

	This can be proved by either of the above inductive methods or
by including %2size_gopher[x.y]_=_size[x.y]%1 in the induction hypothesis
%2ok[x,y]%1.

	The statement about samefringe is

!!n17:	%2∀x y.(issexp samefringe[x,y] ∧ samefringe[x,y] = T ≡ fringe x =
fringe y)%1,

and it is most easily proved by induction on %2size_x_+_size_y%1 using
the predicate

!!n18:	%2P(n) ≡ ∀x y.(n = size x + size y ⊃ issexp samefringe[x,y] ∧
(samefringe[x,y] = T ≡ fringe x = fringe y))%1.

It can also be proved using the well-foundedness of lexicographic ordering
of the list %2<x qa x>%1, but then we must decide what lexicographic orderings
to include in our axiom system.

	Transfinite induction is also useful, and can be illustrated
with a variant %2samefringe%1 that does everything in one complicated
recursive definition, namely

!!n19:	%2samefringe[x,y] = (x equal y) or not aat x and not aat y and
[qif qat qa x qthen [qif qat y qthen qa x equal qa y and
samefringe[qd x, qd y] qelse samefringe[x, qaa y . [qda y . qd y]]]
qelse samefringe[qaa x . [qda x .qd x], y]%1.

The transfinite induction predicate then has the form

!!n20:	%2P(n) ≡ ∀x y.[n = %Aw%*(size x + size y) + size qa x + size qa y ⊃
issexp samefringe[x,y] ∧ (samefringe[x,y] = T ≡ fringe x = fringe y)]%1.

	An easier example requiring induction up to %Aw%52%1 is proving
the termination of Ackermann's function which has the functional
equation

!!20a:	%2∀m n.(A(m,n) = qif m = 0 qthen n+1 qelse qif n = 0 qthen
A(m-1,0) qelse A(m-1,A(m,n-1)))%1.

The statement to be proved is

!!20b:	%2∀α.(α < %Aw%52%2 ∧ α = %Aw%2m + n ⊃ isint A(m,n))%1.

The proof is straightforward, because %Aw%2(m-1)_<_%Aw%2m+n%1 and
%Aw%2m+(n-1)_<_%Aw%2m+n%1, so we can assume %2isint_A(m-1,0)%1
and %2isint_A(m,n-1)%1.  From the latter, it follows that
%Aw%2(m-1)+A(m,n-1)_<_%Aw%2m+n%1 which completes the induction step.

	We would like to prove that the amount of storage used in the
computation of %2samefringe[x,y]%1 aside from that occupied by ⊗x and ⊗y, 
never exceeds the sum of the numbers of %2car%1s required to reach
corresponding atoms in ⊗x and ⊗y.  Unfortunately, we can't even express
that fact, because we are axiomatizing the programs as functions,
and the amount of storage used does not depend merely on the function
being computed; it depends on the method of computation.  We may regard
such things as %2intensional%1 properties, but any correspondence with
the notion of
intensional properties in intensional logic remains to be established.
.bb "#. The Minimization Schema."

	The functional equation of a program doesn't completely
characterize it.  For example, the program

!!h9a:	%2f1 x ← f1 x%1

leads to the sentence

!!h10:	%2∀x.(f1 x = f1 x)%1

which provides no information although the function ⊗f 
is undefined for all ⊗x.  This is not always the case, since
the program

!!h11:	%2f2 x ← (f2 x).qnil%1

has the functional equation

!!h12:	%2∀x.(f2 x = (f2 x).qnil)%1.

from which %2∀x.¬issexp f2(x)%1 can be proved by induction.

	In order to characterize recursive programs, we need some
way of asking for the least defined solution of the functional equation.

	Suppose the program is

!!h13:	%2f x ← %At%*[f](x)%1

yielding the functional equation

!!h14:	%2∀x.(f x = %At%*[f](x)%1.

The %2minimization schema%1 is then

!!h15:	%2∀x.(isD %At%*[%Af%*](x) ⊃ %Af%* x = %At%*[%Af%*](x)) ⊃ ∀x.(isD f x ⊃ %Af%* x = f x)%1,

where the predicate %2isD%1 asserts that its argument is in the domain %2D%1.

	The %2minimization schema%1 can be abbreviated by introducing
Scott's partial ordering q≤ on D%5+%1.  We define

!!h15a:	%2∀X Y.(X q≤ Y ≡ X = qw ∨ X = Y)%1,

so that the only proper ordering is that qw is less than everything else.
We also use the symbol q≥.
The minimization schema then becomes

!!h15b:  %2∀x.(qt[qf](x) q≤ qf(x)) ⊃ ∀x.(f(x) q≤ qf(x))%1,

which makes it more apparent that the minimization schema asserts that
⊗f is minimal.

	In the %2subst%1 example, the schema is

!!h16a:	%2∀x y z.(qf(x,y,z) q≥ qif qat z qthen (qif z = y qthen x qelse z)
qelse qf(x,y,qa z).qf(x,y,qd z)) ⊃ ∀x y z.(qf(x,y,z) q≥ subst(x,y,z))%1,

which has also the longer form

!!h16:	%2∀x y z.(issexp (qif qat z qthen (qif z = y qthen x qelse z)
qelse %Af%*(x,y,qa z).%Af%*(x,y,qd z)) ⊃ (%Af%*(x,y,z) = qif qat z qthen
(qif z = y qthen x qelse z) qelse %Af%*(x,y,qa z).%Af%*(x,y,qd z))) ⊃
∀x y z.(issexp subst(x,y,z) ⊃ %Af%*(x,y,z) = subst(x,y,z))%1.

	In the schema %Af%* is a free function variable of the appropriate
number of arguments.  The schema is just a translation into first order
logic of Park's (1970) theorem

!!h17:	%2%Af%* %8d%2 %At%*[%Af%*] ⊃ %Af%* %8d%2 Y[%At%*]%1.

	The simplest application of the schema is to show that the ⊗f1 
defined by ({eq h9a}) is never an S-expression.  The schema becomes

!!h18:	%2∀x.(%Af%* x q≥ %Af%* x) ⊃ ∀x.(%Af%* x q≥ f1 x)%1,

and we take

!!h19:	%2%Af%* x = qw%1.

The left side of ({eq h18}) is identically true, and, remembering that qw
is not an S-expression, the right side tells us that %2f1 x%1 is never
an S-expression.

	The minimization schema can sometimes be used to show partial
correctness.  For example, the well known 91-function is defined by
the recursive program over the integers

!!h20:	%2f91 x ← qif x > 100 qthen x - 10 qelse f91 f91(x + 11)%1.

The goal is to show that

!!h22:	%2∀x.(f91 x = qif x > 100 qthen x - 10 qelse 91)%1.

We apply the minimization schema with

!!h21:	%2%Af%* x ← qif x > 100 qthen x - 10 qelse 91%1,

and it can be shown by an explicit calculation without induction that
the premiss of the schema is satisfied, and this shows that ⊗f91, 
whenever defined has the desired value.

	The method of recursion induction (McCarthy 1963) is also
an immediate application of the minimization schema.  If we show
that two functions satisfy the schema of a recursive program, we
show that they both equal the function computed by the program on
whereever the function is defined.

	The utility of the minimization schema for proving partial
correctness or non-termination depends on our ability to name
suitable comparison functions.  f1 and f91 were easily treated,
because the necessary comparison functions could be given explicitly
without recursion.  Any extension of the language that provides new
tools for naming comparison functions, e.g. going to higher order
logic, will improve our ability to use the schema in proofs.

	({eq h15}) can be regarded as an axiom schema involving
a second order function variable %At%1.  What can be substituted
for %At%1 is a  quantifier free
λ-expression in a first order function variable.
It may be interesting to study the sets of first order sentences that
can be generated by such second order sentence schemata.  Presumably,
sets of sentences can be generated in this way that cannnot be
generated by schemata with only first order function variables.
.skip 1
.bb "#. Proof Methods as Axiom Schemata"

	Representing recursive definitions in first order logic permits
us to express some well known methods for proving partial correctness
as axiom schemata of first order logic.

	For example, suppose we want to prove that if the input ⊗x of a
function ⊗f defined by

!!c1:	%2f x ← qif p x qthen x qelse f h x%1

satisfies %2%AF%2(x)%1, then if the function terminates, the output %2f(x)%1
will satisfy %AY%2(x,f(x))%1.  We appeal to the following %2axiom schema of
inductive assertions%1:

!!c2:	%2∀x.(%AF%2(x) ⊃ q(x,x)) ∧ ∀x y.(q(x,y) ⊃ qif p x qthen %AY%2(x,y)
qelse q(x,%8 %2h y))
.nofill
		⊃ ∀x.(%AF%2(x) ∧ isD f x ⊃ %AY%2(x,f x))%1

.fill
where %2isD f x%1 is the assertion that %2f(x)%1 is in the nominal
range of the function definition, i.e. is an integer or an S-expression
as the case may be, and asserts that the computation terminates.
In order to use the schema, we must invent a suitable predicate %2q(x,y)%1,
and this is precisely the method of inductive assertions.
The schema is valid for all predicates %AF%1, %AY%1, and %2q%1, and a
similar schema can be written for any collection of mutually recursive
definitions that is iterative.

	The method of %2subgoal induction%1 for recursive programs
was introduced in
(Manna and Pnueli 1970), but they didn't give it a name.
Morris and Wegbreit (1977) name it, extend it somewhat,
and apply it to Algol-like programs.
Unlike %2inductive assertions%1, it isn't
limited to iterative definitions.  Thus, for the
recursive program

!!c3:	%2f%45%2 x ← qif p x qthen h x qelse g1 f%45%2 g2 x%1,

where ⊗p is assumed total, we have

!!c4:	%2∀x.(p x ⊃ q(x,h x)) ∧ ∀x z.(¬p(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧
∀x.(%AF%2(x) ∧ q(x,z) ⊃ %AY%2(x,z))
.nofill
		⊃ ∀x.(%AF%2(x) ∧ isD(f(x)) ⊃ %AY%2(x,f(x)))%1
.fill

	We can express these methods as axiom schemata,
because we have the predicate %2isD%1 to express termination.
The minimization schema itself can be proved by subgoal induction.
We need only take %2%AF%2(x)_≡_%3true%1 and %AY%2(x,y)_≡_(y_=_%Af%2(x))%1
and %2q(x,y)_≡_(y_=_%Af%2(x))%1.

	General rules for going from a recursive program to what amounts
to the subgoal induction schema are given in
(Manna and Pnueli 1970) and (Morris and Wegbreit 1977);
we need only add a conclusion involving
the %2isD%1 predicate to the Manna's and Pnueli formula %2W%4P%1.

	However, we can characterize subgoal induction
as an axiom schema.  Namely, we define %At%2'[q]%1 as an extension of %At%1
mapping relations into relations.  Thus if

!!c5:	%2%At%2[f](x) = qif p x qthen h x qelse g1 f g2 x%1,

we have

!!c6:	%2%At%2'[q](x,y) ≡ qif p x qthen (y = h x) qelse ∃z.(q(g2 x,z) ∧ y = g1 z)%1.

In general we have

!!c7:	%2∀xy.(%At%2'[q](x,y) ⊃ q(x,y)) ⊃ ∀x.(isD f x ⊃ q(x,f x))%1,

from which the subgoal induction rule follows immediately given the properties
of %AF%1 and %AY%1.  I am indebted to Wolfgang Polak (oral communication)
for help in elucidating this relationship.

%3WARNING%1: The rest of this section is still somewhat conjectural
and is subject to change.  There may be bugs.

	The extension %2qt'[q]%1 can be determined as follows:
Introduce into the logic the notion of a %2multi-term%1 which is formed in
the same way as a term but allows relations written as functions.
For the present we won't interpret them but merely give rules for
introducing them and subsequently eliminating them again to get
an ordinary formula.  Thus
we will write ⊗q<e> where ⊗e is any term or multi-term.  We then form %2qt'[q]%1
exactly in the same way %2qt[f]%1 was formed.  Thus for the 91-function
we have

!!c8:	%2qt'[q](x) = qif x>100 qthen x-10 qelse q<q<x+11>>%1.

The pointy brackets indicate that we are "applying" a relation.
We now evaluate %2qt'[q](x,y)%1 formally as follows:

!!c9:	%2qt'[q](x,y)	≡ (qif x>100 qthen x-10 qelse q<q<x+11>>)(y)

			≡ qif x>100 qthen y = x-10 qelse q(q<x+11>,y)

			≡ qif x>100 qthen y = x-10 qelse ∃z.(q(x+11,z) ∧
q(z,y))%1.

This last formula has no pointy brackets and is just the formula that would
be obtained by Manna and Pnueli or Morris and Wegbreit.  The rules are
as follows:

	(i) %2qt'[q](x)%1 is just like %2qt[f](x)%1 except that ⊗q replaces
⊗f and takes its arguments in pointy brackets.

	(ii) an ordinary term ⊗e applied to ⊗y becomes %2y_=_e%1.

	(ii) %2q<e>(y)%1 becomes %2q(e,y)%1.

	(ii) %2P(q<e>)%1 becomes %2∃z.q(e,z)_∧_P(z)%1 when
%2P(q<e>)%1 occurs positively in %2qt'[q](x,y)%1 and becomes
%2∀z.q(e,z)_⊃_P(z)%1 when the occurrence is negatve.
It is not evident what independent semantics should be given to
multi-terms.
.skip 2
.bb "#. Representations Using Finite Approximations."

	Our second approach to representing recursive programs
by first order formulas goes back to Goedel (1931, 1934) who showed
that primitive recursive functions could be so represented.  (Our
knowledge of Goedel's work comes from (Kleene 1951)).

.turn on "α"
.eq←0
	Kleene (1951) calls a function ⊗f %2representable%1 if there
is an arithmetic formula ⊗A with free variables ⊗x and ⊗y such
that

!!b1:	%2∀x_y.((y_=_f(x))_≡_A)%1,

where an arithmetic formula is built up from integer constants and
variables using only addition, multiplication and bounded quantification.
Kleene showed that all partial recursive functions are representable.
The proof involves Goedel numbering possible computation sequences
and showing that the relation between sequences and their elements
and the steps of the computation are all representable.

	In Lisp less machinery is needed, because sequences
are Lisp data, and the relation between a sequence and its elements
is given by basic Lisp functions and by the %2occurence relation%1
defined in section 5 by

!!b2:	%2occur[x,y] ← (x = y) ∨ ¬qat y ∧ [occur[x,qa y] ∨ occur[x, qd y]]%1.

	%2occur%1 is the only recursive definition we shall require.
Since it is total, we only need its functional equation to represent
it in first order logic.  The functional equation is

L17:	%2∀x y.(occur[x,y] ≡ (x=y) ∨ ¬qat y ∧ (occur[x,qa y] ∨ occur[x,qd y]))%1,

	The axiom system consisting of L1-L17, B1-B12, and the sentences
resulting from the schemata LS1 and LS2 will be called the axiom system
Lisp1.

	Starting with %2occur%1 and the basic Lisp functions and
predicates we will define three other Lisp predicates without recursion.
By %2u_istail_v%1 we mean that ⊗u can be obtained from ⊗v by repeated
%2cdr%1s.  Thus the tails of (A B C D) are (A B C D), (B C D), (C D),
(D) and NIL.  The natural recursive definition of %2istail%1 is

!!b3a:	%2u istail v ← (u = v) ∨ (¬qn v ∧ u istail qd v)%1

which according to the previous sections would lead to the first order
formula

!!b3b:	%2∀u v.(u istail v ≡ (u = v) ∨ (¬qn v ∧ u istail qd v))%1,

but ({eq b3b}) is still an implicit definition of %2istail%1, because
the function being defined occurs on both sides of the equivalence
sign.  A suitable explicit definition is

!!b3:	%2∀u v.(u istail v ≡ occur[u,v] ∧ ∀x.(occur[u,x] ∧ occur[x,v]
⊃ x = u ∨ occur[u, qd x]))%1.

Next we shall define membership in a list.  We have

!!b4:	%2∀x v.(x ε v ≡ ∃u.(u istail v ∧ x = qa u))%1.

Now we define an %2a-list%1 - a familiar Lisp concept.  We have

!!b5:	%2∀w.(isalist w ≡ ∀x.(x ε w ⊃ ¬qat x) ∧ ∀u1 u2.(u1 istail w ∧
u2 istail w ∧ qaa u1 = qaa u2 ⊃ u1 = u2))%1.

Thus an %2a-list%1 is a list of pairs such that no S-expression is the
first element of two different pairs.  Therefore, a-lists are suitable for
representing finite lists of argument-value pairs for partial functions.

	Finally, we need the familiar Lisp function %2assoc%1 that is used
for looking up atoms on %2a-lists%1.  Its familiar recursive definition
is

!!b6:	%2assoc(x,w) ← qif qn w qthen qnil qelse qif x = qaa w qthen qa w
qelse assoc(x,qd w)%1,

but it can be represented by

!!b7:	%2∀w x y.(x.y = assoc(x,w) ≡ ∃w1.(w1 istail w ∧ x.y = qa w1)
∨ assoc(x,w) = qnil)%1.

	Now let ⊗f be an arbitrary recursive program defined by

!!b8:	%2f x ← %At%*[f](x)%1

for some continuous functional qt.
In order to emphasize the parallel between a partial function %2f%1 and
an %2a-list%1 used as a finite approximation, we define

!!b8a:	%At%2'(w)(x) = %At%2[λz.qif qn assoc(z,w) qthen qw
qelse qd assoc(z,w)](x)%1.

Thus %At%1' is like %At%1 except that whenever %At%1 evaluates its functional
argument ⊗f at some value ⊗z, %At%1' looks up ⊗z on the a-list ⊗w. 

	With this preparation we can write

!!b9:	%2∀x (¬∃y w.(x.y = qa w ∧ ∀x1 y1 w1.(w1 istail w
∧ x1.y1 = qa w1 ⊃ y1 = %At%2'[qd w1](x1))) ⊃ f(x) = qw) ∧
∀y.(∃w.(x.y = qa w ∧ ∀x1 y1 w1.(w1 istail w
∧ x1.y1 = qa w1 ⊃ y1 = %At%2'[qd w1](x1)))) ⊃ f(x) = y))%1.

	The essence of this formula is simple.  ⊗w is an a-list
containing all argument-value pairs that arise in the evaluation of ⊗f(x). 
We require that if ⊗x occurs somewhere on ⊗w, the pairs involved in the
evaluation of ⊗f(x) occur further on in the a-list ⊗w.  This is to avoid
allowing circular recursions.  If there is no such a-list, then
%2f(x)_=_qw.

	If the logic has a description operator %Ai%1, where
%Ai%2 x.P(x)%1 stands for the "the unique ⊗x such that ⊗P(x) if
there is such a unique ⊗x and otherwise qw", then ({eq b9}) can
be written

!!b9a:	%2∀x.(f(x) = %Ai%2 y.∃w.(x.y = qa w ∧ ∀x1 y1 w1.(w1 istail w
∧ x1.y1 = qa w1 ⊃ y1 = %At%2'[qd w1](x1))))%1.

	As an example, consider the Lisp function %2ff%1 defined
recursively by

!!b10:	%2ff x ← qif qat x qthen x qelse ff qa x%1.

({eq b9a}) then takes the form

!!b11:	∀x.(ff x = %Ai%2y.∃w.(x.y = qa w ∧ ∀x1 y1 w1.(w1 istail w
∧ x1.y1 = qa w1 ⊃ y1 = qif qat x1 qthen x1 qelse (qif qn assoc(x1,qd w1)
qthen qw qelse qd assoc(x1,qd w1)))))%1.

	Suppose we were computing %2ff_((A.B).C)%1.  A suitable ⊗w would
be ((((A.B).C).A) ((A.B).A) (A.A)).

	It might be asked whether %2occur%1 is necessary.  Couldn't we
represent recursive programs using just %2car, cdr, cons%1 and %2atom%1?
No, for the following reason.
Suppose that the function ⊗f is representable using only the basic Lisp
functions without %2subexp%1, and consider the sentence

!!b12:	%2∀x.issexp_f(x)%1,

asserting the totality of ⊗f. 
Using the representation, we can write ({eq b12}) as a sentence
involving only the basic Lisp functions and the constant qw.
However, may be shown in Appendix I, these sentences are decidable,
and totality isn't.  (I'll put the proof in Appendix I if I can
prove it.  At this time, I think I've almost got it).

	In case of functions of several variables,
({eq b9}) corresponds to a call-by-value
computation rule while the representations of the previous sections correspond
to call-by-name or other "safe" rules.  The difference is not important, because
of Vuillemin's theorem that any strict function may be computed either according
to call-by-name or call-by-value.
.BB "#. Questions of Incompleteness."

	Luckham, Park and Paterson (1970) have shown that whether a
program schema diverges for every interpretation, whether it diverges
for some interpretation, and whether two program schemas are equivalent
are all not even partially solvable problems.  Manna (1974) has a
thorough discussion of these points.  In view of these results, what
can be expected from our first order representations?

	First let us construct a Lisp computation that does not terminate,
but whose non-termination cannot be proved from the axioms Lisp1 within
first order logic.  We need only program a proof-checker for first order
logic, set it to generate all possible proofs starting with the axioms Lisp1,
and stop when it finds a proof of (qnil ≠ qnil) or some other contradiction.
Assuming the axioms are consistent, the program will never find such a
proof and will never stop.  In fact, proving that the program will never
stop is precisely proving that the axioms are consistent.  But Goedel's
theorem asserts that axiom systems like Lisp1 cannot be proved consistent
within themselves.
All the known cases of terminating computations that
can't be proved not to terminate within Peano arithmetic
involve such an appeal to Goedel's theorem
or similar unsolvability arguments.

	We can presumably prove Lisp1 consistent
just as Gentzen proved arithmetic consistent - by introducing
a new axiom schema that allows induction up to the transfinite ordinal
ε%40%1.  Proving the new system consistent would require induction up to
a still higher ordinal, etc.

	Since every recursively defined function can be defined explicitly,
any sentence involving such functions can be replaced by an equivalent
sentence involving only %2occur%1 and the basic Lisp functions.
The theory of %2occur%1 and these functions has a standard model, the
usual S-expressions and many non-standard models.  We "construct"
non-standard models in the usual way by appealing to the theorem that
if every finite subset of a set ⊗S of sentences of first order logic
has a model, then ⊗S has a model.
For example, take %2S = α{occur[qnil, x], occur[%1(A)%2, x], occur[%1(A A)%2
, x], ...%1 indefinitelyα}.  Every finite subset of ⊗S has a model;
we need only take ⊗x to be the longest list of A's occurring in the
sentences.
Hence there is a model of the Lisp axioms in which ⊗x has all lists
of A's as subexpressions.  No sentence true in the standard model
and false in such a model can be proved from the axioms.  However,
it is necessary to be careful about the meaning of termination of a
function.  In fact, taking successive %2cdr%1s of such an ⊗x would
never terminate, but the sentence whose %2standard interpretation%1
is termination of the computation is provable from Lisp1.

	The practical question is: where does the correctness of ordinary
programs come in?  It seems likely that such statements will be provable
with our original system of axioms.  It doesn't follow that the system
Lisp1 will permit convenient proofs, but probably it will.  Some heuristic
evidence for this comes from (Cohen 1965).  Cohen presents two systems
of axiomatized arithmetic Z1 and Z2.  Z1 is ordinary Peano arithmetic with
an axiom schema of induction, and Z2 is an axiomatization of hereditarily
finite sets of integers.  Superficially, Z2 is more powerful than Z1, but
because the set operations of Z2 can be represented in Z1 as functions
on the Goedel numbers of the sets, it turns out that Z1 is just as powerful
once the necessary machinery has been established.  Because sets and lists
are the basic data of Lisp1, and sets are easily represented, the power of Lisp1
will be approximately that of Z2, and convenient proofs of correctness
statements should be possible.  
Moreover, since Lisp1 is a first order theory, it is easily extended
with axioms for sets, and this should help make informal proofs easy to
express.
It would be nice to be able to express these
considerations less vaguely.
.bb "#. References."

%3Cartwright, R.S. (1977)%1:
%2A Practical Formal Semantic Definition and Verification System
for Typed Lisp%1,
Ph.D. Thesis, Computer Science Department, Stanford University,
Stanford, California.

%3Cohen, Paul (1966)%1: %2Set Theory and the Continuum Hypothesis%1,
W.A. Benjamin Inc.

%3Cooper, D.C. (1969)%1: "Program Scheme Equivalences and Second-order
Logic", in B. Meltzer and D. Michie (eds.), %2Machine Intelligence%1,
Vol. 4, pp. 3-15, Edinburgh University Press, Edinburgh.

%3Kleene, S.C. (1951)%1: %2Introduction to Metamathematics%1,
Van Nostrand, New York.

%3Luckham, D.C., D.M.R.Park, and M.S. Paterson (1970)%1: "On Formalized
Computer Programs", %2J. CSS%1, %34%1(3): 220-249 (June).

%3Manna, Zohar and Amir Pnueli (1970)%1: "Formalization of the Properties
of Functional Programs", %2J. ACM%1, %317%1(3): 555-569.

%3Manna, Zohar (1974)%1: %2Mathematical Theory of Computation%1,
McGraw-Hill.

%3Manna, Zohar, Stephen Ness and Jean Vuillemin (1973)%1: "Inductive Methods
for Proving Properties of Programs", %2Comm. ACM%1,%316%1(8): 491-502 (August).

%3McCarthy, John%1 (1963) "A Basis for a Mathematical Theory of Computation", in
P. Braffort and D. Hirschberg (eds.), %2Computer Programming and Formal Systems%1,
pp. 33-70.  North-Holland Publishing Company, Amsterdam.

%3Morris, James H., and Ben Wegbreit (1977)%1: "Program Verification
by Subgoal Induction", %2Comm. ACM%1,%320%1(4): 209-222 (April).

%3Park, David (1969)%1: Fixpoint Induction and Proofs of Program
Properties", in %2Machine Intelligence 5%1, pp. 59-78, Edinburgh
University Press, Edinburgh.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end